M:MsgA, l:IdLnk, tg:Id. M.dout2(l;tg)  Type 

latex

Definitions	M.dout2(l;tg), MsgA, locl(a), IdDeq, 1of(t), x. t(x), Top, 2of(t), Prop, Valtype(da;k), State(ds), f(x)?z, a:A fp B(a), Knd, KindDeq, rcv(l,tg), x:A. B(x), Id, t  T, IdLnk
Lemmas	IdLnk wf, Id wf, rcv wf, Kind-deq wf, top wf, fpf wf, pi2 wf, fpf-cap wf, pi1 wf, ma-valtype wf, ma-state wf, id-deq wf, locl wf, Knd wf, msga wf